Inference at * 1 2 1 2 1 1 1 
Iof proof for Lemma fast-fib:



1. n : 
2. 0 < n
3. a, b:.
3. {m:| 
3. {k:.
3. {(a = fib(k))  ((k  0)  (b = 0))  ((0 < k)  (b = fib(k - 1)))  (m = fib((n - 1)+k))} 
4. a : 
5. b : 
6. b1:.
6. {m:| 
6. {k:.
6. {(a+b = fib(k))
6. { ((k  0)  (b1 = 0))
6. { ((0 < k)  (b1 = fib(k - 1)))
6. { (m = fib((n - 1)+k))} 
7. m : 
8. k:.
8. (a+b = fib(k))  ((k  0)  (a = 0))  ((0 < k)  (a = fib(k - 1)))  (m = fib((n - 1)+k))
9. k : 
10. a = fib(k)
11. (k  0)  (b = 0)
12. (0 < k)  (b = fib(k - 1))
13. k = 0
  a+b = fib(0+1) 

latex

 by ((D (11)) 
CollapseTHEN (Auto)) 
CollapseTHEN (((if (first_bool T:b
C) then HypSubst' else RevHypSubst') ( -1)( 0))) 

latex

C1: 

C1: 11. (0 < k)  (b = fib(k - 1))
C1: 12. k = 0
C1: 13. b = 0
C1:   a+0 = fib(0+1)
C.

Definitions

x:AB(x), Void, a < b, n+m, , {x:A| B(x)} , A  B, A, False, s ~ t, fib(n), , s = t, , SQType(T), x:A. B(x), P  Q, {T}, t  T